Nuprl Lemma : rng_times_one
13,42
postcript
pdf
r
:Rng,
a
:|
r
|. (
a
* 1) =
a
& (1 *
a
) =
a
latex
Up
rings
1
Definitions of Statement
Rng
,
r
xmn
Definitions
t
T
,
x
:
A
.
B
(
x
)
,
t
.2
,
t
.1
,
r
xmn
,
e
,
*
,
|
g
|
Lemmas
rng
wf
,
mul
mon
of
rng
wf
c
,
mon
ident
origin
r:Rng, a:|r|. (a * 1) = a & (1 * a) = a r:Rng, a:|r|. (a * 1) = a & (1 * a) = a 
xmn
Tx:A. B(x)xmn